1. Field
The field of the present invention relates to verification technology of digital designs, and in particular, to a method and system for implementing context aware synthesis of assertions.
2. Description of Related Art
Assertion Based Verification (ABV) is widely used in the electronics industry for functional verification. ABV has become a mainstream verification technology of digital designs. IEEE 1850 PSL (Property Specification Language) and IEEE 1800 SVA (System Verilog Assertions) are standard languages for specifying assertions in ABV. In ABV assertions written in PSL or SVA are verified by various verification tools. Assertions describe the behavior of circuits at a high level of abstraction. These need to be synthesized to finite state machines for verification tools to verify them. In addition, these may need to be synthesized to Deterministic Finite Automata (DFA) and Non-deterministic Finite Automata (NFA) for verification tools to use them.
In general, techniques to synthesize PSL and SVA are not readily addressed in literature. The generally known LTL (Linear Time Logic) formula to automata generation for model checking does not apply directly to PSL and SVA assertion synthesis. In PSL and SVA, complexity is added over and above LTL due to the presence of sequences and local-variables. In general, a sequence defines temporal behavior and has constructs over and above regular expressions. This adds requirements on PSL and SVA assertion synthesis.
The performance of formal verification degrades exponentially with increase in size of the Finite State Machines (FSM) corresponding to assertions, and the performance of emulation and simulation degrades with increase in size of FSMs. Thus, assertion synthesis generates FSMs with a least possible number of states.